| 1: | nats_active | → add_active(zeros_active) | |
| 2: | hd_active(x) | → hd(x) | |
| 3: | zeros_active | → cons(0,zeros) | |
| 4: | tl_active(x) | → tl(x) | |
| 5: | incr_active(cons(x,y)) | → cons(s(x),incr(y)) | |
| 6: | mark(nats) | → nats_active | |
| 7: | add_active(cons(x,y)) | → incr_active(cons(x,add(y))) | |
| 8: | mark(zeros) | → zeros_active | |
| 9: | hd_active(cons(x,y)) | → mark(x) | |
| 10: | mark(incr(x)) | → incr_active(mark(x)) | |
| 11: | tl_active(cons(x,y)) | → mark(y) | |
| 12: | mark(add(x)) | → add_active(mark(x)) | |
| 13: | nats_active | → nats | |
| 14: | mark(hd(x)) | → hd_active(mark(x)) | |
| 15: | zeros_active | → zeros | |
| 16: | mark(tl(x)) | → tl_active(mark(x)) | |
| 17: | incr_active(x) | → incr(x) | |
| 18: | mark(0) | → 0 | |
| 19: | add_active(x) | → add(x) | |
| 20: | mark(s(x)) | → s(x) | |
| 21: | mark(cons(x,y)) | → cons(x,y) | |
| 22: | NATS_ACTIVE | → ADD_ACTIVE(zeros_active) | |
| 23: | NATS_ACTIVE | → ZEROS_ACTIVE | |
| 24: | MARK(nats) | → NATS_ACTIVE | |
| 25: | ADD_ACTIVE(cons(x,y)) | → INCR_ACTIVE(cons(x,add(y))) | |
| 26: | MARK(zeros) | → ZEROS_ACTIVE | |
| 27: | HD_ACTIVE(cons(x,y)) | → MARK(x) | |
| 28: | MARK(incr(x)) | → INCR_ACTIVE(mark(x)) | |
| 29: | MARK(incr(x)) | → MARK(x) | |
| 30: | TL_ACTIVE(cons(x,y)) | → MARK(y) | |
| 31: | MARK(add(x)) | → ADD_ACTIVE(mark(x)) | |
| 32: | MARK(add(x)) | → MARK(x) | |
| 33: | MARK(hd(x)) | → HD_ACTIVE(mark(x)) | |
| 34: | MARK(hd(x)) | → MARK(x) | |
| 35: | MARK(tl(x)) | → TL_ACTIVE(mark(x)) | |
| 36: | MARK(tl(x)) | → MARK(x) | |